(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const r1 Real)
(declare-const r14 Real)
(declare-const r16 Real)
(declare-const v17 Bool)
(declare-const v19 Bool)
(declare-const r23 Real)
(declare-const v21 Bool)
(assert (or (not (= v8 (distinct 14.0 6382.0 3950665.0 56656.0 0.0) v3 v17 (= v11 v11 v0) v13 v6 (not v12) (xor (>= r14 0.0) v6 v11 v13) (= 0.93412570 r1 r1 2371.0))) (not (= v8 (distinct 14.0 6382.0 3950665.0 56656.0 0.0) v3 v17 (= v11 v11 v0) v13 v6 (not v12) (xor (>= r14 0.0) v6 v11 v13) (= 0.93412570 r1 r1 2371.0))) (distinct r16 (/ (/ 3688.0 r1) r16) 9668.1971 3726.0)))
(assert (or (< r14 3688.0 3726.0 0.93412570 r16) v12 (=> v21 v17)))
(assert (or v7 (> 56656.0 72.0) (not (= v8 (distinct 14.0 6382.0 3950665.0 56656.0 0.0) v3 v17 (= v11 v11 v0) v13 v6 (not v12) (xor (>= r14 0.0) v6 v11 v13) (= 0.93412570 r1 r1 2371.0)))))
(assert (or v12 (> 56656.0 72.0) (> 56656.0 72.0)))
(check-sat)
